<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>WorkVarManager</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="WorkVarManager";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/lang/WorkVarHyp.html" title="class in mmj.lang"><span class="strong">Prev Class</span></a></li>
<li>Next Class</li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/lang/WorkVarManager.html" target="_top">Frames</a></li>
<li><a href="WorkVarManager.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.lang</div>
<h2 title="Class WorkVarManager" class="title">Class WorkVarManager</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li>mmj.lang.WorkVarManager</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<hr>
<br>
<pre>public class <span class="strong">WorkVarManager</span>
extends java.lang.Object</pre>
<div class="block">WorkVarManager is a "helper" class that is used to define, declare, alloc and
 maintain state information about a set of Work Variables.</div>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/lang/WorkVarManager.html#WorkVarManager(mmj.verify.Grammar)">WorkVarManager</a></strong>(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar)</code>
<div class="block">Sole constructor for WorkVarManager.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/WorkVar.html" title="class in mmj.lang">WorkVar</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/WorkVarManager.html#alloc(mmj.lang.Cnst)">alloc</a></strong>(<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;typ)</code>
<div class="block">Allocates a new WorkVar for the input Type Code.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/WorkVar.html" title="class in mmj.lang">WorkVar</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/WorkVarManager.html#alloc(java.lang.String)">alloc</a></strong>(java.lang.String&nbsp;workVarIn)</code>
<div class="block">Allocates the WorkVar specified by the input token if necessary assuming
 it is a valid WorkVar token string.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/WorkVar.html" title="class in mmj.lang">WorkVar</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/WorkVarManager.html#alloc(mmj.lang.WorkVar)">alloc</a></strong>(<a href="../../mmj/lang/WorkVar.html" title="class in mmj.lang">WorkVar</a>&nbsp;workVar)</code>
<div class="block">Allocates a given WorkVar.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/WorkVarHyp.html" title="class in mmj.lang">WorkVarHyp</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/WorkVarManager.html#allocWorkVarHyp(mmj.lang.Cnst)">allocWorkVarHyp</a></strong>(<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;typ)</code>
<div class="block">Allocates a new WorkVar for the input Type Code and returns the
 corresponding WorkVarHyp.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/WorkVarManager.html#areWorkVarsDeclared()">areWorkVarsDeclared</a></strong>()</code>
<div class="block">Returns true if the Work Variables have been declared.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/WorkVarManager.html#dealloc(mmj.lang.WorkVar)">dealloc</a></strong>(<a href="../../mmj/lang/WorkVar.html" title="class in mmj.lang">WorkVar</a>&nbsp;workVar)</code>
<div class="block">Deallocates a WorkVar.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/WorkVarManager.html#dealloc(mmj.lang.WorkVarHyp)">dealloc</a></strong>(<a href="../../mmj/lang/WorkVarHyp.html" title="class in mmj.lang">WorkVarHyp</a>&nbsp;workVarHyp)</code>
<div class="block">Deallocates a WorkVar given a WorkVarHyp</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/WorkVarManager.html#deallocAll()">deallocAll</a></strong>()</code>
<div class="block">Deallocates all Work Variables.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/WorkVarManager.html#deallocAndReallocAll(mmj.pa.ProofWorksheet)">deallocAndReallocAll</a></strong>(<a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a>&nbsp;w)</code>&nbsp;</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/WorkVarManager.html#declareWorkVars(mmj.verify.Grammar, mmj.lang.LogicalSystem)">declareWorkVars</a></strong>(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
               <a href="../../mmj/lang/LogicalSystem.html" title="class in mmj.lang">LogicalSystem</a>&nbsp;logicalSystem)</code>
<div class="block">Declare the Work Variables that have been defined.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/WorkVarManager.html#defineWorkVarType(mmj.verify.Grammar, java.lang.String, java.lang.String, int)">defineWorkVarType</a></strong>(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
                 java.lang.String&nbsp;grammaticalTypCdIn,
                 java.lang.String&nbsp;workVarPrefixIn,
                 int&nbsp;nbrWorkVarsIn)</code>
<div class="block">Define the Work Variables to be used for a given grammatical type code.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/WorkVarManager.html#editGrammaticalTypCd(mmj.verify.Grammar, java.lang.String)">editGrammaticalTypCd</a></strong>(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
                    java.lang.String&nbsp;grammaticalTypCdIn)</code>
<div class="block">Validates an input string as being a valid Type Code for Work Variables.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>java.lang.Integer</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/WorkVarManager.html#editNbrWorkVars(int)">editNbrWorkVars</a></strong>(int&nbsp;nbrWorkVarsIn)</code>
<div class="block">Validates an input string specifying the number of WorkVar objects to be
 declared for a specific Type Code.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/WorkVarManager.html#editWorkVarPrefix(java.lang.String)">editWorkVarPrefix</a></strong>(java.lang.String&nbsp;workVarPrefixIn)</code>
<div class="block">Validates an input string as being a valid WorkVar Prefix.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/WorkVarManager.html#isAllocated(mmj.lang.WorkVar)">isAllocated</a></strong>(<a href="../../mmj/lang/WorkVar.html" title="class in mmj.lang">WorkVar</a>&nbsp;workVar)</code>
<div class="block">Returns true if input Work Var is allocated.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/WorkVarManager.html#resolveWorkVarUpdates()">resolveWorkVarUpdates</a></strong>()</code>
<div class="block">Deallocates Work Vars that have updates and eliminates chains of WorkVar
 updates so that a Work Var update subtree contains only non-updated Work
 Vars.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/WorkVarManager.html#setPrevAllocNbr(mmj.lang.Cnst, int)">setPrevAllocNbr</a></strong>(<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;typ,
               int&nbsp;prevAllocNbr)</code>
<div class="block">Sets the value of prevAllocIndex for a Type Code.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="WorkVarManager(mmj.verify.Grammar)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>WorkVarManager</h4>
<pre>public&nbsp;WorkVarManager(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar)</pre>
<div class="block">Sole constructor for WorkVarManager.
 <p>
 Does nothing except allocate the Arraylists to hold input definitions.
 Note therefore that the WorkVarManager object is not ready for use by
 ProofAsst or elsewhere until the Work Variables are actually declared,
 and a NullPointerException will result if access is attempted before
 then.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>grammar</code> - Grammar object for loaded .mm file.</dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="areWorkVarsDeclared()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>areWorkVarsDeclared</h4>
<pre>public&nbsp;boolean&nbsp;areWorkVarsDeclared()</pre>
<div class="block">Returns true if the Work Variables have been declared.
 <p>
 If no Work Variable definitions are input and the Proof Assistant is
 instantiated prior to declaration of Work Variables, ProofAsstBoss.java
 will declare the Work Variables using the default definitions. Which is
 why we need this function...</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>true if Work Variables declared yet.
         <p></dd></dl>
</li>
</ul>
<a name="defineWorkVarType(mmj.verify.Grammar, java.lang.String, java.lang.String, int)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>defineWorkVarType</h4>
<pre>public&nbsp;void&nbsp;defineWorkVarType(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
                     java.lang.String&nbsp;grammaticalTypCdIn,
                     java.lang.String&nbsp;workVarPrefixIn,
                     int&nbsp;nbrWorkVarsIn)
                       throws <a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></pre>
<div class="block">Define the Work Variables to be used for a given grammatical type code.
 <p>
 The definitions are stored separately from the tables constructed by
 "Declare". This allows mixing of definitions and default values for Work
 Variables.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>grammar</code> - Grammar object for loaded .mm file.</dd><dd><code>grammaticalTypCdIn</code> - String holding the Cnst used as a Type Code
            (e.g. "wff").</dd><dd><code>workVarPrefixIn</code> - String holding the prefix to be used with a
            numeric suffix to name Work Variables of a given Type.</dd><dd><code>nbrWorkVarsIn</code> - number of Work Variables to declare for this Type
            Code.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></code> - if individual field values are invalid.</dd></dl>
</li>
</ul>
<a name="declareWorkVars(mmj.verify.Grammar, mmj.lang.LogicalSystem)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>declareWorkVars</h4>
<pre>public&nbsp;void&nbsp;declareWorkVars(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
                   <a href="../../mmj/lang/LogicalSystem.html" title="class in mmj.lang">LogicalSystem</a>&nbsp;logicalSystem)
                     throws <a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></pre>
<div class="block">Declare the Work Variables that have been defined.
 <p>
 The input definitions and default values for each grammatical Type Code
 are used to create the Work Variable objects and finalize the
 WorkVarManager object for actual use.
 <p>
 Note that final validation checks are performed to ensure that there are
 no duplicate Var or VarHyp names, either among the Work Variable objects
 or the other symbols and statements defined in the LogicalSystem for the
 input .mm file. This means checking for duplicate Work Var prefixes as
 well as checking each WorkVar and WorkVarHyp name against the
 LogicalSystem's Symbol and Statement tables.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>grammar</code> - Grammar object for loaded .mm file.</dd><dd><code>logicalSystem</code> - LogicalSystem for loaded .mm file.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></code> - if duplicate Var or VarHyp names result or if
             there is a conflict with the Symbol and Statement table
             namespaces.</dd></dl>
</li>
</ul>
<a name="editGrammaticalTypCd(mmj.verify.Grammar, java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>editGrammaticalTypCd</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;editGrammaticalTypCd(<a href="../../mmj/verify/Grammar.html" title="class in mmj.verify">Grammar</a>&nbsp;grammar,
                        java.lang.String&nbsp;grammaticalTypCdIn)
                          throws <a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></pre>
<div class="block">Validates an input string as being a valid Type Code for Work Variables.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>grammar</code> - Grammar object for loaded .mm file.</dd><dd><code>grammaticalTypCdIn</code> - String Type Code (Cnst)</dd>
<dt><span class="strong">Returns:</span></dt><dd>Cnst Type Code.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></code> - if input Type Code invalid.</dd></dl>
</li>
</ul>
<a name="editWorkVarPrefix(java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>editWorkVarPrefix</h4>
<pre>public&nbsp;java.lang.String&nbsp;editWorkVarPrefix(java.lang.String&nbsp;workVarPrefixIn)
                                   throws <a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></pre>
<div class="block">Validates an input string as being a valid WorkVar Prefix.
 <p>
 Duplicate checking is not done here, just checking to make sure that the
 input prefix characters are valid Metamath "math symbols".</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>workVarPrefixIn</code> - String of Metamath math symbols.</dd>
<dt><span class="strong">Returns:</span></dt><dd>workVarPrefix string, trimmed.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></code> - if workVarPrefixIn has non math symbols or is
             null or empty.</dd></dl>
</li>
</ul>
<a name="editNbrWorkVars(int)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>editNbrWorkVars</h4>
<pre>public&nbsp;java.lang.Integer&nbsp;editNbrWorkVars(int&nbsp;nbrWorkVarsIn)
                                  throws <a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></pre>
<div class="block">Validates an input string specifying the number of WorkVar objects to be
 declared for a specific Type Code.
 <p>
 Basically this is just a range check: greater than some number (9) and
 less than some other number (999).</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>nbrWorkVarsIn</code> - Number of WorkVar objects for a given Type Code.</dd>
<dt><span class="strong">Returns:</span></dt><dd>nbrWorkVars input int converted to Integer (for storage in
         ArrayList).</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></code> - if nbrWorkVarsIn out of range.</dd></dl>
</li>
</ul>
<a name="isAllocated(mmj.lang.WorkVar)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>isAllocated</h4>
<pre>public&nbsp;boolean&nbsp;isAllocated(<a href="../../mmj/lang/WorkVar.html" title="class in mmj.lang">WorkVar</a>&nbsp;workVar)</pre>
<div class="block">Returns true if input Work Var is allocated.
 <p>
 Note: this is a weird function, since how could an unallocated WorkVar be
 input to see whether or not it is allocates? BUT... consult
 <a href="../../mmj/pa/StepUnifier.html#finalizeAndLoadAssrtSubst()"><code>StepUnifier.finalizeAndLoadAssrtSubst()</code></a> for explanatory
 remarks...</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>workVar</code> - the Work Var to check</dd>
<dt><span class="strong">Returns:</span></dt><dd>true if input Work Var is allocated.</dd></dl>
</li>
</ul>
<a name="resolveWorkVarUpdates()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>resolveWorkVarUpdates</h4>
<pre>public&nbsp;void&nbsp;resolveWorkVarUpdates()</pre>
<div class="block">Deallocates Work Vars that have updates and eliminates chains of WorkVar
 updates so that a Work Var update subtree contains only non-updated Work
 Vars.
 <p>
 Processing is by Type Code, in reverse order by Work Var number within
 Type Code so that subsequent alloc() calls begin with the lowest
 deallocated Work Var numbers.
 <p>
 Example: WorkVar "A" where = B and B = C results in update clone of
 A.paSubst: A = C.</div>
</li>
</ul>
<a name="alloc(java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>alloc</h4>
<pre>public&nbsp;<a href="../../mmj/lang/WorkVar.html" title="class in mmj.lang">WorkVar</a>&nbsp;alloc(java.lang.String&nbsp;workVarIn)</pre>
<div class="block">Allocates the WorkVar specified by the input token if necessary assuming
 it is a valid WorkVar token string.
 <p>
 If the WorkVar is already allocated it just returns the WorkVar instance.
 <p>
 The input String must consist of a prefix which matches one of the
 specified WorkVar prefixes, followed by a positive integer within the
 range of WorkVar numbers specified for the Type Code corresponding to the
 prefix.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>workVarIn</code> - token specifying a WorkVar (id)</dd>
<dt><span class="strong">Returns:</span></dt><dd>allocated WorkVar or null.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code>java.lang.IllegalArgumentException</code> - if workVarIn is null or an empty String.</dd></dl>
</li>
</ul>
<a name="alloc(mmj.lang.WorkVar)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>alloc</h4>
<pre>public&nbsp;<a href="../../mmj/lang/WorkVar.html" title="class in mmj.lang">WorkVar</a>&nbsp;alloc(<a href="../../mmj/lang/WorkVar.html" title="class in mmj.lang">WorkVar</a>&nbsp;workVar)</pre>
<div class="block">Allocates a given WorkVar.
 <p>
 It is hard to envision using this function...</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>workVar</code> - to be allocated.</dd>
<dt><span class="strong">Returns:</span></dt><dd>allocated WorkVar.</dd></dl>
</li>
</ul>
<a name="allocWorkVarHyp(mmj.lang.Cnst)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>allocWorkVarHyp</h4>
<pre>public&nbsp;<a href="../../mmj/lang/WorkVarHyp.html" title="class in mmj.lang">WorkVarHyp</a>&nbsp;allocWorkVarHyp(<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;typ)
                           throws <a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></pre>
<div class="block">Allocates a new WorkVar for the input Type Code and returns the
 corresponding WorkVarHyp.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>typ</code> - Cnst Type Code of WorkVar to be allocated.</dd>
<dt><span class="strong">Returns:</span></dt><dd>allocated WorkVar's WorkVarHyp.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></code> - if no remaining WorkVar objects are available for
             use with the given Type Code.</dd></dl>
</li>
</ul>
<a name="alloc(mmj.lang.Cnst)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>alloc</h4>
<pre>public&nbsp;<a href="../../mmj/lang/WorkVar.html" title="class in mmj.lang">WorkVar</a>&nbsp;alloc(<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;typ)
              throws <a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></pre>
<div class="block">Allocates a new WorkVar for the input Type Code.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>typ</code> - Cnst Type Code of WorkVar to be allocated.</dd>
<dt><span class="strong">Returns:</span></dt><dd>allocated WorkVar.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/VerifyException.html" title="class in mmj.lang">VerifyException</a></code> - if no remaining WorkVar objects are available for
             use with the given Type Code.</dd></dl>
</li>
</ul>
<a name="deallocAndReallocAll(mmj.pa.ProofWorksheet)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>deallocAndReallocAll</h4>
<pre>public&nbsp;void&nbsp;deallocAndReallocAll(<a href="../../mmj/pa/ProofWorksheet.html" title="class in mmj.pa">ProofWorksheet</a>&nbsp;w)</pre>
</li>
</ul>
<a name="deallocAll()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>deallocAll</h4>
<pre>public&nbsp;void&nbsp;deallocAll()</pre>
<div class="block">Deallocates all Work Variables.</div>
</li>
</ul>
<a name="dealloc(mmj.lang.WorkVarHyp)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>dealloc</h4>
<pre>public&nbsp;void&nbsp;dealloc(<a href="../../mmj/lang/WorkVarHyp.html" title="class in mmj.lang">WorkVarHyp</a>&nbsp;workVarHyp)</pre>
<div class="block">Deallocates a WorkVar given a WorkVarHyp</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>workVarHyp</code> - workVarHyp to be deallocated.</dd></dl>
</li>
</ul>
<a name="dealloc(mmj.lang.WorkVar)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>dealloc</h4>
<pre>public&nbsp;void&nbsp;dealloc(<a href="../../mmj/lang/WorkVar.html" title="class in mmj.lang">WorkVar</a>&nbsp;workVar)</pre>
<div class="block">Deallocates a WorkVar.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>workVar</code> - to be deallocated.</dd></dl>
</li>
</ul>
<a name="setPrevAllocNbr(mmj.lang.Cnst, int)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>setPrevAllocNbr</h4>
<pre>public&nbsp;void&nbsp;setPrevAllocNbr(<a href="../../mmj/lang/Cnst.html" title="class in mmj.lang">Cnst</a>&nbsp;typ,
                   int&nbsp;prevAllocNbr)</pre>
<div class="block">Sets the value of prevAllocIndex for a Type Code.
 <p>
 In other words, if we input '1' for &W1, then the next allocation will be
 &W2.
 <p>
 If the input prevAllocNbr is invalid a default setting of zero is used
 instead.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>typ</code> - Cnst Type Code of prevAllocIndex to set.</dd><dd><code>prevAllocNbr</code> - is one greater than prevAllocIndex</dd></dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/lang/WorkVarHyp.html" title="class in mmj.lang"><span class="strong">Prev Class</span></a></li>
<li>Next Class</li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/lang/WorkVarManager.html" target="_top">Frames</a></li>
<li><a href="WorkVarManager.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
